active(c) → mark(f(g(c)))
active(f(g(X))) → mark(g(X))
mark(c) → active(c)
mark(f(X)) → active(f(X))
mark(g(X)) → active(g(X))
f(mark(X)) → f(X)
f(active(X)) → f(X)
g(mark(X)) → g(X)
g(active(X)) → g(X)
↳ QTRS
↳ DependencyPairsProof
active(c) → mark(f(g(c)))
active(f(g(X))) → mark(g(X))
mark(c) → active(c)
mark(f(X)) → active(f(X))
mark(g(X)) → active(g(X))
f(mark(X)) → f(X)
f(active(X)) → f(X)
g(mark(X)) → g(X)
g(active(X)) → g(X)
F(mark(X)) → F(X)
MARK(f(X)) → ACTIVE(f(X))
MARK(c) → ACTIVE(c)
MARK(g(X)) → ACTIVE(g(X))
ACTIVE(c) → F(g(c))
ACTIVE(f(g(X))) → MARK(g(X))
ACTIVE(c) → G(c)
G(active(X)) → G(X)
ACTIVE(c) → MARK(f(g(c)))
G(mark(X)) → G(X)
F(active(X)) → F(X)
active(c) → mark(f(g(c)))
active(f(g(X))) → mark(g(X))
mark(c) → active(c)
mark(f(X)) → active(f(X))
mark(g(X)) → active(g(X))
f(mark(X)) → f(X)
f(active(X)) → f(X)
g(mark(X)) → g(X)
g(active(X)) → g(X)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
F(mark(X)) → F(X)
MARK(f(X)) → ACTIVE(f(X))
MARK(c) → ACTIVE(c)
MARK(g(X)) → ACTIVE(g(X))
ACTIVE(c) → F(g(c))
ACTIVE(f(g(X))) → MARK(g(X))
ACTIVE(c) → G(c)
G(active(X)) → G(X)
ACTIVE(c) → MARK(f(g(c)))
G(mark(X)) → G(X)
F(active(X)) → F(X)
active(c) → mark(f(g(c)))
active(f(g(X))) → mark(g(X))
mark(c) → active(c)
mark(f(X)) → active(f(X))
mark(g(X)) → active(g(X))
f(mark(X)) → f(X)
f(active(X)) → f(X)
g(mark(X)) → g(X)
g(active(X)) → g(X)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
G(active(X)) → G(X)
G(mark(X)) → G(X)
active(c) → mark(f(g(c)))
active(f(g(X))) → mark(g(X))
mark(c) → active(c)
mark(f(X)) → active(f(X))
mark(g(X)) → active(g(X))
f(mark(X)) → f(X)
f(active(X)) → f(X)
g(mark(X)) → g(X)
g(active(X)) → g(X)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
G(active(X)) → G(X)
G(mark(X)) → G(X)
The value of delta used in the strict ordering is 4.
POL(active(x1)) = 1 + x_1
POL(mark(x1)) = 4 + (4)x_1
POL(G(x1)) = (4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
active(c) → mark(f(g(c)))
active(f(g(X))) → mark(g(X))
mark(c) → active(c)
mark(f(X)) → active(f(X))
mark(g(X)) → active(g(X))
f(mark(X)) → f(X)
f(active(X)) → f(X)
g(mark(X)) → g(X)
g(active(X)) → g(X)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
F(mark(X)) → F(X)
F(active(X)) → F(X)
active(c) → mark(f(g(c)))
active(f(g(X))) → mark(g(X))
mark(c) → active(c)
mark(f(X)) → active(f(X))
mark(g(X)) → active(g(X))
f(mark(X)) → f(X)
f(active(X)) → f(X)
g(mark(X)) → g(X)
g(active(X)) → g(X)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F(mark(X)) → F(X)
F(active(X)) → F(X)
The value of delta used in the strict ordering is 4.
POL(active(x1)) = 1 + x_1
POL(mark(x1)) = 4 + (4)x_1
POL(F(x1)) = (4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
active(c) → mark(f(g(c)))
active(f(g(X))) → mark(g(X))
mark(c) → active(c)
mark(f(X)) → active(f(X))
mark(g(X)) → active(g(X))
f(mark(X)) → f(X)
f(active(X)) → f(X)
g(mark(X)) → g(X)
g(active(X)) → g(X)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
MARK(f(X)) → ACTIVE(f(X))
MARK(g(X)) → ACTIVE(g(X))
ACTIVE(f(g(X))) → MARK(g(X))
active(c) → mark(f(g(c)))
active(f(g(X))) → mark(g(X))
mark(c) → active(c)
mark(f(X)) → active(f(X))
mark(g(X)) → active(g(X))
f(mark(X)) → f(X)
f(active(X)) → f(X)
g(mark(X)) → g(X)
g(active(X)) → g(X)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
MARK(f(X)) → ACTIVE(f(X))
Used ordering: Polynomial interpretation [25,35]:
MARK(g(X)) → ACTIVE(g(X))
ACTIVE(f(g(X))) → MARK(g(X))
The value of delta used in the strict ordering is 8.
POL(active(x1)) = (2)x_1
POL(MARK(x1)) = (4)x_1
POL(f(x1)) = 2 + (4)x_1
POL(g(x1)) = 0
POL(mark(x1)) = 2 + (4)x_1
POL(ACTIVE(x1)) = 0
g(active(X)) → g(X)
g(mark(X)) → g(X)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
MARK(g(X)) → ACTIVE(g(X))
ACTIVE(f(g(X))) → MARK(g(X))
active(c) → mark(f(g(c)))
active(f(g(X))) → mark(g(X))
mark(c) → active(c)
mark(f(X)) → active(f(X))
mark(g(X)) → active(g(X))
f(mark(X)) → f(X)
f(active(X)) → f(X)
g(mark(X)) → g(X)
g(active(X)) → g(X)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
ACTIVE(f(g(X))) → MARK(g(X))
Used ordering: Polynomial interpretation [25,35]:
MARK(g(X)) → ACTIVE(g(X))
The value of delta used in the strict ordering is 1/64.
POL(active(x1)) = 0
POL(MARK(x1)) = (1/4)x_1
POL(f(x1)) = 1/4 + (1/4)x_1
POL(g(x1)) = 1/4
POL(mark(x1)) = 0
POL(ACTIVE(x1)) = (1/4)x_1
g(active(X)) → g(X)
g(mark(X)) → g(X)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
MARK(g(X)) → ACTIVE(g(X))
active(c) → mark(f(g(c)))
active(f(g(X))) → mark(g(X))
mark(c) → active(c)
mark(f(X)) → active(f(X))
mark(g(X)) → active(g(X))
f(mark(X)) → f(X)
f(active(X)) → f(X)
g(mark(X)) → g(X)
g(active(X)) → g(X)